Translate Flux Bool to Prop in Lean and open Classical everywhere#1527
Translate Flux Bool to Prop in Lean and open Classical everywhere#1527ranjitjhala merged 3 commits intomainfrom
Conversation
| fn lean_fmt(&self, f: &mut fmt::Formatter, cx: &LeanCtxt) -> fmt::Result { | ||
| let FunDef { name, sort, comment: _, body } = self; | ||
| write!(f, "def ")?; | ||
| write!(f, "noncomputable def ")?; |
There was a problem hiding this comment.
Is this necessary as soon as you open Classical, or do you need it for some specific functions?
|
Really it’s for specific functions, but I don’t think it’s something we can
tell in advance, so I thought putting it in by default is the safe way to
go. Maybe we could put it only on generated files (because the user can’t
go fix them if we get it wrong), and let the user fix the error if it comes
up in user-edited files.
…On Mon, Mar 2, 2026 at 15:50 Nico Lehmann ***@***.***> wrote:
***@***.**** commented on this pull request.
------------------------------
In crates/flux-infer/src/lean_format.rs
<#1527 (comment)>:
> @@ -559,7 +526,7 @@ impl LeanFmt for Expr {
impl LeanFmt for FunDef {
fn lean_fmt(&self, f: &mut fmt::Formatter, cx: &LeanCtxt) -> fmt::Result {
let FunDef { name, sort, comment: _, body } = self;
- write!(f, "def ")?;
+ write!(f, "noncomputable def ")?;
Is this necessary as soon as you open Classical, or do you need it for
some specific functions?
—
Reply to this email directly, view it on GitHub
<#1527 (review)>,
or unsubscribe
<https://github.com/notifications/unsubscribe-auth/AHOC4BLTZGOFLKBICW2MGMD4OYM4JAVCNFSM6AAAAACWEYNJUOVHI2DSMVQWIX3LMV43YUDVNRWFEZLROVSXG5CSMV3GSZLXHMZTQNZZGQZDCNBSGE>
.
You are receiving this because you authored the thread.Message ID:
***@***.***>
|
|
Did you put |
I put it almost everywhere. I didn't put it on the declarations we make for interpreted rust constants (because I think it's unlikely it'd be required). Let me tinker with it a little and figure out whether other declarations need it, if I had to guess right now I'd say functions definitely require it, theorems, and proofs might sometimes require it, sort declarations probably don't require it. Update after some more reading, I think only functions should have it.
|
nilehmann
left a comment
nilehmann
left a comment
There was a problem hiding this comment.
This is closer to what I was expecting. A little sad that we have to mark all functions as noncomputable, but I suppose that's the price we are paying for going classical. We can revisit later...
|
Yes, lets try this out and if it hits glitches we can always do the more fine-grained thing... |
3 participants
noncomputableto stop lean from complaining if they indeed happen to be non-computableTODOtest this out a littleI'm slightly concerned that the translation might break down when bools appear in non-positive positions, but I don't know of a useful reason we'd do thatTested by emitting lean files in
flux-demo(for sorting related PCs). It seems to work fine. The second point I'm still not sure about, but I think LEM would allow us to do what we need.